\requiere{registrada(m, c1)}
\requiere{registrada(m, c2)}
\requiere{compatibles(m, c1, c2)}
%\requiere{noCompartenProvincias(m, c1, c2)}

\modifica{m}
\asegura{(\forall hoteles \selec cadenasDeHoteles(m))(\nexists h \selec hoteles) cadena(h) == c2}
\asegura{(\forall hoteles \selec cadenasDeHoteles(m))(\\ 
\IfThenElse{(\exists h \selec hoteles) cadena(h) == c1 \\}
{mismos(hoteles, hotelesDeCadena(pre(m), c1) ++ hotelesDeCadena(pre(m), c2) \\}
{mismos(hoteles, hotelesDeCadena(pre(m), cadena(hotel[0])})}

\asegura{mismoNombreCadena(m, fusionados(pre(m), c1, c2))}
\asegura{\neg registrada(m, c2)}
\asegura{mismos(secretarias(m), secretarias(pre(m))}
\asegura{todos(\comp{mismos(registro(m, secretarias(m)[i]), registro(pre(m), secretarias(pre(m))[i]))}{
\\ i \selec \rangoca{0}{|secretarias(m)|}})}

\asegura{todos(\comp{\\ \IfThenElse{cadena(registro(pre(m), secretarias(pre(m))[i])[j]) == c2 \\}{
cadena(registro(m, secretarias(m)[i])[j]) == c2 \\}{
cadena(registro(m, secretarias(m)[i])[j]) == cadena(registro(pre(m), secretarias(pre(m))[i])[j])}}{
\\ i \selec \rangoca{0}{|secretarias(m)|}, 
   j \selec registro(m, secretarias(m)[i])})}

\aux{mismoNombreCadena}{m : MinisterioDeTurismo, c : [Hotel]}{\bool}{
\\ \comp{todos({\comp{cadena(hotel) == c}{hotel \selec cadena}})}{cadena \selec cadenasDeHoteles(m), cadena(c[0]) == c}[0]}

\aux{fusionados}{m: MinisterioDeTurismo, c1, c2: Cadena}{[Hotel]}{hotelesDeCadena(m, c1) ++ hotelesDeCadena(m, c2)} 

%\aux{renombrarCadena}{hs : [Hotel], c : Cadena}{[Hotel]}{}

\aux{cadena}{m : MinisterioDeTurismo, nombre : Cadena}{[Hotel]}{\comp{c}{c \selec cadenasDeHoteles(m), cadena(c[0]) == nombre}}

\aux{compatibles}{m: MinisterioDeTurismo, c1, c2: Cadena}{\bool}{\\ 
todos(\comp{nombre(h1) \neq nombre(h2)}{h1, h2 \selec hotelesDeCadena(c1) ++ hotelesDeCadena(c2), h1 \neq h2}) \wedge \\
sinRepetidos(\comp{hotel}{hotel \selec hotelesDeCadena(c1) ++ hotelesDeCadena(c2)}) \wedge \\
sinRepetidos(\comp{provinciaDeHotel(hotel)}{hotel \selec hotelesDeCadena(c1) ++ hotelesDeCadena(c2)}) }

\aux{registrada}{m : MinisterioDeTurismo, c : Cadena}{\bool}{c \in nombresCadenas(m)}	

\aux{nombresCadenas}{m : MinisterioDeTurismo}{[Cadena]}{\\ sacarRepetidos(\comp{cadena(hotel)}{cadena \selec cadenasDeHoteles(m), hotel \selec cadena})}

\aux{provinciaDeHotel}{m : MinisterioDeTurismo, nombreh : String}{[Provincia]}{
\\ \comp{provincia}{provincia \selec secretarias(m),
\\ hotel \selec registro(m, provincia), 
\\ nombre(hotel) == nombreh}[0]}
